\begin{tabbing}
$\forall$${\it es}$:ES, $e$, ${\it e'}$:E.
\\[0ex]isrcv($e$)
\\[0ex]$\Rightarrow$ isrcv(${\it e'}$)
\\[0ex]$\Rightarrow$ (\=$e$ $=$ ${\it e'}$\+
\\[0ex]$\Leftrightarrow$
\\[0ex]sender($e$) $=$ sender(${\it e'}$) $\in$ E \& lnk($e$) $=$ lnk(${\it e'}$) $\in$ IdLnk \& index($e$) $=$ index(${\it e'}$) $\in$ $\mathbb{Z}$)
\-
\end{tabbing}